; <lemma>
;  <title>BoschSwitch.4</title>
;  <origin>BoschSwitch | trm1 | TriggerOn/inv4/INV</origin>
(benchmark boschswitch_4
;  <theories>
;    <theory name="linear_order_int"/>
;    <theory name="basic_set"/>
;  </theories>
  :logic AUFLIA
;  <typenv>
;    <variable name="S" type="POW(INTEGER)"/>
  :extrapreds (
		(S Int)
		)
;    <variable name="i" type="INTEGER"/>
;  </typenv>
  :extrafuns (
	       (i Int) 
	       )
  :extramacros (
		 (Nat
		  (lambda (?i Int) . (<= 0 ?i)))
		 (in (lambda (?x 't) (?p ('t boolean)) . (?p ?x)))
		 (subseteq
		   (lambda (?p ('t boolean)) (?q ('t boolean)) .
		     (forall (?x 't). 
		       (implies (?p ?x) (?q ?x)))))
		 )
; <hypothesis needed="true">S : POW(NATURAL)</hypothesis>
  :assumption (subseteq S Nat)
; <hypothesis needed="true">i : S</hypothesis>
  :assumption (in i S)
; <goal>i : NATURAL</goal>
  :formula
  (not
      (in i Nat)
    )
)
; </lemma>
